$\forall$${\it es}$:ES, $e$:E, $x$:Id. state when $e$$\backslash\backslash$$x$ $\in$ state@loc($e$)$\backslash\backslash$$x$